<html>
<head><meta charset="utf-8"><title>meeting 2021-03-23 · project-const-generics · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/index.html">project-const-generics</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html">meeting 2021-03-23</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="231478057"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231478057" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231478057">(Mar 23 2021 at 14:22)</a>:</h4>
<p><span class="user-group-mention" data-user-group-id="3805">@project-const-generics</span> meeting in 23 minutes</p>



<a name="231481293"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231481293" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231481293">(Mar 23 2021 at 14:42)</a>:</h4>
<p>meeting notes: <a href="https://hackmd.io/ApIfCRWSQEa0insNCkNZ-w">https://hackmd.io/ApIfCRWSQEa0insNCkNZ-w</a></p>



<a name="231481388"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231481388" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231481388">(Mar 23 2021 at 14:42)</a>:</h4>
<p>i want to talk a bit more about how we deal with complex generic constants</p>



<a name="231481492"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231481492" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231481492">(Mar 23 2021 at 14:43)</a>:</h4>
<p>so something like <code>fn foo&lt;T: Trait&gt;() where [u8; &lt;T as Trait&gt;::ASSOC]: OtherTrait {}</code></p>



<a name="231482159"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231482159" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231482159">(Mar 23 2021 at 14:47)</a>:</h4>
<p>well, then <span aria-label="sparkles" class="emoji emoji-2728" role="img" title="sparkles">:sparkles:</span> let's officially start this meeting</p>



<a name="231482540"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231482540" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231482540">(Mar 23 2021 at 14:49)</a>:</h4>
<p>the first issue i want to talk about is <a href="#narrow/stream/260443-project-const-generics/topic/anon.20const.20in.20where.20bounds">https://rust-lang.zulipchat.com/#narrow/stream/260443-project-const-generics/topic/anon.20const.20in.20where.20bounds</a></p>



<a name="231482581"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231482581" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231482581">(Mar 23 2021 at 14:49)</a>:</h4>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="cp">#![feature(const_generics, const_evaluatable_checked)]</span><span class="w"></span>

<span class="k">trait</span><span class="w"> </span><span class="n">Foo</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="k">type</span> <span class="nc">Assoc</span><span class="p">;</span><span class="w"></span>
<span class="w">    </span><span class="k">const</span><span class="w"> </span><span class="n">ASSOC</span>: <span class="o">&lt;</span><span class="bp">Self</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="n">Foo</span><span class="o">&gt;</span>::<span class="n">Assoc</span><span class="p">;</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>

<span class="k">impl</span><span class="w"> </span><span class="n">Foo</span><span class="w"> </span><span class="k">for</span><span class="w"> </span><span class="kt">i32</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="k">type</span> <span class="nc">Assoc</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="kt">i64</span><span class="p">;</span><span class="w"></span>
<span class="w">    </span><span class="k">const</span><span class="w"> </span><span class="n">ASSOC</span>: <span class="kt">i64</span> <span class="o">=</span><span class="w"> </span><span class="mi">3</span><span class="p">;</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>

<span class="k">const</span><span class="w"> </span><span class="k">fn</span> <span class="nf">bar</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">(</span><span class="n">x</span>: <span class="nc">T</span><span class="p">)</span><span class="w"> </span>-&gt; <span class="kt">usize</span> <span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">std</span>::<span class="n">mem</span>::<span class="n">forget</span><span class="p">(</span><span class="n">x</span><span class="p">);</span><span class="w"></span>
<span class="w">    </span><span class="mi">3</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>

<span class="k">fn</span> <span class="nf">foo</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">()</span><span class="w"> </span><span class="k">where</span><span class="w"></span>
<span class="w">    </span><span class="n">T</span>: <span class="nc">Foo</span><span class="o">&lt;</span><span class="n">Assoc</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">T</span><span class="o">&gt;</span><span class="p">,</span><span class="w"></span>
<span class="w">    </span><span class="p">[</span><span class="kt">u8</span><span class="p">;</span><span class="w"> </span><span class="n">bar</span>::<span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">(</span><span class="o">&lt;</span><span class="n">T</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="n">Foo</span><span class="o">&gt;</span>::<span class="n">ASSOC</span><span class="p">)]</span>: <span class="nb">Sized</span><span class="p">,</span><span class="w"></span>
<span class="p">{}</span><span class="w"></span>

<span class="k">fn</span> <span class="nf">main</span><span class="p">()</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">foo</span>::<span class="o">&lt;</span><span class="kt">i32</span><span class="o">&gt;</span><span class="p">();</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>



<a name="231482711"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231482711" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231482711">(Mar 23 2021 at 14:50)</a>:</h4>
<p>in <code>main</code> we call <code>foo::&lt;i32&gt;</code></p>



<a name="231482787"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231482787" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231482787">(Mar 23 2021 at 14:51)</a>:</h4>
<p><code>i32: Foo&lt;Assoc = i32&gt;</code> does not hold, so this snippet should fail to compile</p>



<a name="231482825"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231482825" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231482825">(Mar 23 2021 at 14:51)</a>:</h4>
<p>we also have a <code>[u8; bar::&lt;T&gt;(&lt;T as Foo&gt;::ASSOC)]: Sized,</code> bound though</p>



<a name="231483063"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231483063" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231483063">(Mar 23 2021 at 14:52)</a>:</h4>
<p>this one causes us to try and evaluate <code>bar::&lt;T&gt;(&lt;T as Foo&gt;::ASSOC)</code></p>



<a name="231483210"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231483210" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231483210">(Mar 23 2021 at 14:53)</a>:</h4>
<p><em>without</em> first checking if the caller-bounds (so <code>where</code>-clauses, the stuff the caller has to prove before executing our constant) hold</p>



<a name="231483349"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231483349" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231483349">(Mar 23 2021 at 14:54)</a>:</h4>
<p>so the constant assumes that <code>T</code> is the same type as <code>&lt;T as Foo&gt;::ASSOC</code> which isn't actually true</p>



<a name="231483394"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231483394" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231483394">(Mar 23 2021 at 14:54)</a>:</h4>
<p>when we try to use <code>foo::&lt;i32&gt;</code>. This currently causes an ICE</p>



<a name="231483505"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231483505" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231483505">(Mar 23 2021 at 14:55)</a>:</h4>
<p>broadly speaking, there are two ways we can solve this afaik:</p>



<a name="231483573"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231483573" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231483573">(Mar 23 2021 at 14:55)</a>:</h4>
<ul>
<li>change mir building/typeck/ctfe so that it does not ice, even if where-clauses don't hold</li>
</ul>



<a name="231483724"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231483724" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231483724">(Mar 23 2021 at 14:56)</a>:</h4>
<ul>
<li>somehow check that the where-clauses hold before trying to evaluate an anon const, even when used as part of its parent where clauses</li>
</ul>



<a name="231483830"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231483830" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231483830">(Mar 23 2021 at 14:57)</a>:</h4>
<p>the first option seems really undesirable to me, as implementing this probably masks a lot of other, actual bugs we want to detect</p>



<a name="231483899"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231483899" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231483899">(Mar 23 2021 at 14:57)</a>:</h4>
<p>while <span class="user-mention" data-user-id="116009">@nikomatsakis</span> expressed that the second one isn't really that feasable if i understood him correctly</p>



<a name="231483939"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231483939" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231483939">(Mar 23 2021 at 14:58)</a>:</h4>
<p>i don't have any ideas on how we would implement the second one</p>



<a name="231484025"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231484025" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231484025">(Mar 23 2021 at 14:58)</a>:</h4>
<p>so nikos assessment might very well be correct</p>



<a name="231484181"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231484181" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231484181">(Mar 23 2021 at 14:59)</a>:</h4>
<p>I'm a bit behind</p>



<a name="231484550"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231484550" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231484550">(Mar 23 2021 at 15:00)</a>:</h4>
<p>Chalk essentially implements the second option by design, right? As it will simply queue up the obligations, and solve each one when it has enough information to know whether it can be satisfied. (The implementation of Chalk isn't fresh in my mind, so I'm pretending Chalk = Prolog-style trait constraint solver; this may lead to my misunderstanding how it actually works.)</p>



<a name="231484693"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231484693" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231484693">(Mar 23 2021 at 15:01)</a>:</h4>
<p>This is an aside; I just want to check this is a problem specifically with how the current rustc system works, and not a fundamental design problem.</p>



<a name="231485263"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231485263" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231485263">(Mar 23 2021 at 15:04)</a>:</h4>
<p>For some reason i'm having trouble deciding what I think about the two options</p>



<a name="231485319"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231485319" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231485319">(Mar 23 2021 at 15:04)</a>:</h4>
<p>let me take another sip of coffee <span aria-label="coffee" class="emoji emoji-2615" role="img" title="coffee">:coffee:</span> and try again</p>



<a name="231485654"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231485654" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231485654">(Mar 23 2021 at 15:06)</a>:</h4>
<p>ok, I'm getting it now</p>



<a name="231485682"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231485682" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231485682">(Mar 23 2021 at 15:06)</a>:</h4>
<p>thanks <span class="user-mention" data-user-id="216206">@lcnr</span> for a crisp example</p>



<a name="231485819"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231485819" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231485819">(Mar 23 2021 at 15:07)</a>:</h4>
<p>this kind of connects to something I was talking over recently in another context</p>



<a name="231486008"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231486008" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231486008">(Mar 23 2021 at 15:08)</a>:</h4>
<p>basically we were talking about the challenge of having to "export" results, and about how sometimes it'd be easier if the solver can just defer solving things until later</p>



<a name="231486114"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231486114" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231486114">(Mar 23 2021 at 15:08)</a>:</h4>
<p><span class="user-mention silent" data-user-id="216206">lcnr</span> <a href="#narrow/stream/260443-project-const-generics/topic/meeting.202021-03-23/near/231483724">said</a>:</p>
<blockquote>
<ul>
<li>somehow check that the where-clauses hold before trying to evaluate an anon const, even when used as part of its parent where clauses</li>
</ul>
</blockquote>
<p>can we dig a bit into this -- like where are the points where we have to evaluate <code>bar::&lt;T&gt;(...)</code></p>



<a name="231486175"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231486175" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231486175">(Mar 23 2021 at 15:09)</a>:</h4>
<p>I feel like there is maybe a third option</p>



<a name="231486186"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231486186" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231486186">(Mar 23 2021 at 15:09)</a>:</h4>
<p>when checking whether the <code>where</code>-clauses of <code>foo</code> hold</p>



<a name="231486251"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231486251" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231486251">(Mar 23 2021 at 15:09)</a>:</h4>
<p>so probably during <code>fulfill</code> when typechecking <code>main</code></p>



<a name="231486280"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231486280" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231486280">(Mar 23 2021 at 15:09)</a>:</h4>
<p>you mean-- when typechecking the body of <code>main</code></p>



<a name="231486295"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231486295" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231486295">(Mar 23 2021 at 15:09)</a>:</h4>
<p>yeah</p>



<a name="231486351"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231486351" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231486351">(Mar 23 2021 at 15:10)</a>:</h4>
<p>put another way, the problem here is that</p>



<a name="231486400"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231486400" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231486400">(Mar 23 2021 at 15:10)</a>:</h4>
<p>we type-check the constant in the context of <code>foo</code></p>



<a name="231486452"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231486452" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231486452">(Mar 23 2021 at 15:10)</a>:</h4>
<p>and it passes the type-check there, but precisely because of this where clause that is in scope</p>



<a name="231486554"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231486554" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231486554">(Mar 23 2021 at 15:11)</a>:</h4>
<p>but then we get an ICE at some later point because we're assuming that the generic constant is well typed post substitution, when in fact this is not true</p>



<a name="231486608"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231486608" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231486608">(Mar 23 2021 at 15:11)</a>:</h4>
<p>I'm thinking about this because it feels like this is not <em>specific</em> to constant evaluation</p>



<a name="231486749"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231486749" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231486749">(Mar 23 2021 at 15:12)</a>:</h4>
<p>i think it is <span aria-label="thinking" class="emoji emoji-1f914" role="img" title="thinking">:thinking:</span> constants are the only things relying on <code>where</code>-clauses while also being part of them</p>



<a name="231486811"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231486811" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231486811">(Mar 23 2021 at 15:13)</a>:</h4>
<p>at least that's what i think is the core of this issue</p>



<a name="231486827"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231486827" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231486827">(Mar 23 2021 at 15:13)</a>:</h4>
<p>the analogous thing would be predicate well-formedness, I think</p>



<a name="231486950"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231486950" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231486950">(Mar 23 2021 at 15:13)</a>:</h4>
<p>does that pose an issue for <code>T::Assoc: OtherTrait</code></p>



<a name="231486966"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231486966" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231486966">(Mar 23 2021 at 15:13)</a>:</h4>
<p>I agree that it's sort of specific to constants in that the trait solver doesn't assume that predicates are well-formed when it goes to solve them, I think</p>



<a name="231487127"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231487127" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231487127">(Mar 23 2021 at 15:14)</a>:</h4>
<p>that's an example I'm pondering</p>



<a name="231487176"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231487176" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231487176">(Mar 23 2021 at 15:14)</a>:</h4>
<p>which also assumes <code>T: Trait</code> to hold, but not really because our typesystem knows how to deal with it</p>



<a name="231487233"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231487233" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231487233">(Mar 23 2021 at 15:14)</a>:</h4>
<p>it also reminds me of implied bounds</p>



<a name="231487261"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231487261" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231487261">(Mar 23 2021 at 15:14)</a>:</h4>
<p>we want to show that the set of where-clauses are true collectively</p>



<a name="231487415"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231487415" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231487415">(Mar 23 2021 at 15:15)</a>:</h4>
<p>I mean one obvious conclusion is that maybe we can't assume constants are well-typed post substitution :)</p>



<a name="231487459"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231487459" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231487459">(Mar 23 2021 at 15:15)</a>:</h4>
<p>that's one of the options</p>



<a name="231487506"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231487506" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231487506">(Mar 23 2021 at 15:15)</a>:</h4>
<p>but it seems unfortunate to give up that guarantee</p>



<a name="231487536"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231487536" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231487536">(Mar 23 2021 at 15:15)</a>:</h4>
<p>it's not a guarantee we ever had, apparently</p>



<a name="231487610"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231487610" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231487610">(Mar 23 2021 at 15:16)</a>:</h4>
<p>we have this guarantee rn</p>



<a name="231487628"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231487628" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231487628">(Mar 23 2021 at 15:16)</a>:</h4>
<p>we don't, hence the ICE :)</p>



<a name="231487671"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231487671" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231487671">(Mar 23 2021 at 15:16)</a>:</h4>
<p>notice the feature gate</p>



<a name="231487719"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231487719" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231487719">(Mar 23 2021 at 15:16)</a>:</h4>
<p>ok, you mean we have it without using a feature gate</p>



<a name="231487721"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231487721" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231487721">(Mar 23 2021 at 15:16)</a>:</h4>
<p>on stable anon consts can't see any where bounds</p>



<a name="231487774"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231487774" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231487774">(Mar 23 2021 at 15:17)</a>:</h4>
<p>ok so I think an analogous example might be</p>



<a name="231487868"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231487868" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231487868">(Mar 23 2021 at 15:17)</a>:</h4>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">fn</span> <span class="nf">foo</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">()</span><span class="w"></span>
<span class="k">where</span><span class="w"></span>
<span class="w">    </span><span class="n">T</span>: <span class="nb">Iterator</span><span class="p">,</span><span class="w"></span>
<span class="w">    </span><span class="o">&lt;</span><span class="n">T</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="nb">Iterator</span><span class="o">&gt;</span>::<span class="n">Item</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="kt">u32</span><span class="p">,</span><span class="w"></span>
</code></pre></div>
<p>this is not legal Rust syntax, but I'm using it to demonstrate a point</p>



<a name="231487959"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231487959" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231487959">(Mar 23 2021 at 15:18)</a>:</h4>
<p>the second assertion only makes sense if <code>T: Iterator</code> holds in the first place</p>



<a name="231488144"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231488144" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231488144">(Mar 23 2021 at 15:19)</a>:</h4>
<p>the nature of "normalizing" an associated type tends to also guarantee that <code>T: Iterator</code> holds, but it doesn't have to</p>



<a name="231488172"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231488172" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231488172">(Mar 23 2021 at 15:19)</a>:</h4>
<p>for example, you could imagine that we find a definition in an impl and we <em>assume</em> the where clauses of the impl hold</p>



<a name="231488189"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231488189" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231488189">(Mar 23 2021 at 15:19)</a>:</h4>
<p>because they ought to be checked somewhere else</p>



<a name="231488377"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231488377" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231488377">(Mar 23 2021 at 15:20)</a>:</h4>
<p>so...it seems like what's missing a bit is that</p>



<a name="231488427"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231488427" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231488427">(Mar 23 2021 at 15:20)</a>:</h4>
<p>we don't have to check that the constant is well-typed post substitution <em>but</em> we do have to check that its where clauses hold before we can evaluate it</p>



<a name="231488545"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231488545" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231488545">(Mar 23 2021 at 15:21)</a>:</h4>
<p>"check that its where clauses" implies "check that the constant is well-typed post substitution"</p>



<a name="231488546"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231488546" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231488546">(Mar 23 2021 at 15:21)</a>:</h4>
<p>but that is a <em>bit</em> cyclic I guess, its where clauses may include itself?</p>



<a name="231488592"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231488592" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Boxy [she/her] <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231488592">(Mar 23 2021 at 15:21)</a>:</h4>
<p>ayyy we're back to cycles</p>



<a name="231488618"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231488618" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231488618">(Mar 23 2021 at 15:22)</a>:</h4>
<p>with <code>feature(const_generics)</code> it does</p>



<a name="231488666"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231488666" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231488666">(Mar 23 2021 at 15:22)</a>:</h4>
<p>well, <span class="user-mention" data-user-id="216206">@lcnr</span>, we checked that its well-typed under the assumption that the where-clauses hold</p>



<a name="231488668"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231488668" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231488668">(Mar 23 2021 at 15:22)</a>:</h4>
<p>but that's already something we have to change</p>



<a name="231488723"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231488723" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231488723">(Mar 23 2021 at 15:22)</a>:</h4>
<p>right, I wanted to revisit that question and remind myself how we were thinking about that</p>



<a name="231488804"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231488804" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231488804">(Mar 23 2021 at 15:22)</a>:</h4>
<p>i think we talked about it in a prev meeting in the context of trying to use itself to prove a predicate while typechecking itself</p>



<a name="231488904"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231488904" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231488904">(Mar 23 2021 at 15:23)</a>:</h4>
<p>I would also add that, with caching, checking things twice is not a big deal -- but cycles could be a problem, at least unless we leverage coinductive semantics . This does feel like a coinductive sort of problem -- wanting to make sure that a set of things are mutually consistent.</p>



<a name="231489044"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231489044" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231489044">(Mar 23 2021 at 15:24)</a>:</h4>
<p>What I remember is that we want to find a base set of where clauses based on -- say -- the type parameters that appear in the constant</p>



<a name="231489078"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231489078" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231489078">(Mar 23 2021 at 15:24)</a>:</h4>
<p>and then we want to use some form of transitive closure algorithm to expand that set</p>



<a name="231489103"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231489103" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231489103">(Mar 23 2021 at 15:24)</a>:</h4>
<p>remind me what the transitive function is</p>



<a name="231489106"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231489106" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231489106">(Mar 23 2021 at 15:24)</a>:</h4>
<p>yes, though that's mostly to remove unused generic params ^^</p>



<a name="231489145"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231489145" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231489145">(Mar 23 2021 at 15:25)</a>:</h4>
<p>the most naive option I can think of virtually guarantees that the constant itself is in the set</p>



<a name="231489245"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231489245" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231489245">(Mar 23 2021 at 15:25)</a>:</h4>
<p>the transitive function is whether params are used together in a where bound</p>



<a name="231489292"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231489292" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231489292">(Mar 23 2021 at 15:25)</a>:</h4>
<p>which means that the constant itself is in the set</p>



<a name="231489306"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231489306" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231489306">(Mar 23 2021 at 15:25)</a>:</h4>
<p>unless we filter it <del>afterwards</del></p>



<a name="231489580"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231489580" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231489580">(Mar 23 2021 at 15:27)</a>:</h4>
<p>time I guess to do some reading up on dependent typing, isn't it</p>



<a name="231489836"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231489836" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231489836">(Mar 23 2021 at 15:28)</a>:</h4>
<p>potentially</p>



<a name="231489841"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231489841" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231489841">(Mar 23 2021 at 15:28)</a>:</h4>
<p>The main point is that option (2) seems to be impossible so long as there are cycles unless we figure out how to resolve those. I suspect there are also cycles that can't fruitfully be filtered, and that's seeming awfully complex.</p>



<a name="231489914"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231489914" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231489914">(Mar 23 2021 at 15:29)</a>:</h4>
<p>(I will add that I've contemplated what it would mean for all of trait solving to be coinductive, but most folks seem to go the other way...)</p>



<a name="231489948"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231489948" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231489948">(Mar 23 2021 at 15:29)</a>:</h4>
<p>(...that is, trying to model coinductive things in an inductive way)</p>



<a name="231489973"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231489973" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231489973">(Mar 23 2021 at 15:29)</a>:</h4>
<p>(coinductive, loosely speaking, means 'cycles are provable' :)</p>



<a name="231490005"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231490005" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231490005">(Mar 23 2021 at 15:29)</a>:</h4>
<p>This seems like it's getting into the territory of "we need a formal treatment of trait solving in Rust".</p>



<a name="231490127"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231490127" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231490127">(Mar 23 2021 at 15:30)</a>:</h4>
<p>let me ask around a bit about this</p>



<a name="231490144"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231490144" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231490144">(Mar 23 2021 at 15:30)</a>:</h4>
<p>coinductive means that <code>(c /\ a -&gt; b) /\ (c /\ b -&gt; a) -&gt; (c -&gt; a)</code>?</p>



<a name="231490234"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231490234" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231490234">(Mar 23 2021 at 15:31)</a>:</h4>
<p><code>-&gt;</code> meaning <em>implies</em> here</p>



<a name="231490302"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231490302" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231490302">(Mar 23 2021 at 15:31)</a>:</h4>
<p>I won't try to answer and will instead point you at some cryptic wikipedia pages</p>



<a name="231490331"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231490331" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231490331">(Mar 23 2021 at 15:31)</a>:</h4>
<p>My experience is that everybody -- including tenured professors -- who you ask about coinduction</p>



<a name="231490342"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231490342" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231490342">(Mar 23 2021 at 15:31)</a>:</h4>
<p>begins by saying "I don't understand it, but..."</p>



<a name="231490452"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231490452" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231490452">(Mar 23 2021 at 15:32)</a>:</h4>
<p>"use it until it becomes intuitive"</p>



<a name="231490468"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231490468" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231490468">(Mar 23 2021 at 15:32)</a>:</h4>
<p>think of auto traits</p>



<a name="231490504"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231490504" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231490504">(Mar 23 2021 at 15:32)</a>:</h4>
<p>it's kind of "greatest fixed point"</p>



<a name="231490601"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231490601" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231490601">(Mar 23 2021 at 15:33)</a>:</h4>
<p>if proving that <code>T: Foo</code> is true requires (recursively) that <code>T: Foo</code> is true, that's ok, so long as you don't encounter anything false along the way</p>



<a name="231490675"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231490675" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231490675">(Mar 23 2021 at 15:34)</a>:</h4>
<p><span aria-label="thumbs up" class="emoji emoji-1f44d" role="img" title="thumbs up">:thumbs_up:</span></p>



<a name="231490706"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231490706" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231490706">(Mar 23 2021 at 15:34)</a>:</h4>
<p>in the case of auto traits, it'd be like, <code>LinkedList&lt;T&gt;: Send</code> if all the types you can reach from <code>LinkedList&lt;T&gt;</code> are <code>Send</code> -- and that includes <code>LinkedList&lt;T&gt;</code> itself!</p>



<a name="231490785"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231490785" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231490785">(Mar 23 2021 at 15:34)</a>:</h4>
<p>but if you're not careful with how you setup your implications you can get into problems</p>



<a name="231490872"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231490872" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231490872">(Mar 23 2021 at 15:35)</a>:</h4>
<p>like clearly if <code>T: Foo =&gt; T: Foo</code> then it is vacuously provable, so you can't have other things implied by <code>T: Foo</code> being true that are not also vacuously provable; we had bugs around autotraits because of this</p>



<a name="231491296"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491296" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491296">(Mar 23 2021 at 15:37)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> <a href="#narrow/stream/260443-project-const-generics/topic/meeting.202021-03-23/near/231490785">said</a>:</p>
<blockquote>
<p>but if you're not careful with how you setup your implications you can get into problems</p>
</blockquote>
<p>adding <code>(a -&gt; a) -&gt; a</code> as an axiom certainly doesn't suffice</p>



<a name="231491318"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491318" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491318">(Mar 23 2021 at 15:37)</a>:</h4>
<p>It would be nice to have a document in the project-const-generics repo, or elsewhere, that lists all these problem cases that have been encountered, so there's a good reference to point people towards in the future.</p>



<a name="231491506"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491506" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491506">(Mar 23 2021 at 15:38)</a>:</h4>
<p>It also seems likely that without a formally verified model of trait solving, it's likely these issues will be hit again and again. Maybe you can tempt an academic into working on it.</p>



<a name="231491529"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491529" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491529">(Mar 23 2021 at 15:38)</a>:</h4>
<p>yes</p>



<a name="231491535"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491535" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491535">(Mar 23 2021 at 15:38)</a>:</h4>
<p>so I think this example</p>



<a name="231491542"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491542" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491542">(Mar 23 2021 at 15:38)</a>:</h4>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">trait</span><span class="w"> </span><span class="n">Foo</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="k">type</span> <span class="nc">Assoc</span><span class="p">;</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>

<span class="k">const</span><span class="w"> </span><span class="k">fn</span> <span class="nf">bar</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">()</span><span class="w"></span>
<span class="k">where</span><span class="w"></span>
<span class="w">    </span><span class="n">T</span>: <span class="nc">Foo</span><span class="o">&lt;</span><span class="n">Assoc</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">T</span><span class="o">&gt;</span><span class="p">,</span><span class="w"></span>
<span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="o">..</span><span class="p">.</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>

<span class="k">fn</span> <span class="nf">fun1</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"></span>
<span class="k">where</span><span class="w"></span>
<span class="w">    </span><span class="n">T</span>: <span class="nc">Foo</span><span class="o">&lt;</span><span class="n">Assoc</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">T</span><span class="o">&gt;</span><span class="p">,</span><span class="w"></span>
<span class="w">    </span><span class="p">[</span><span class="kt">u8</span><span class="p">;</span><span class="w"> </span><span class="n">bar</span>::<span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">()]</span>: <span class="nb">Sized</span><span class="p">,</span><span class="w"></span>
<span class="p">{}</span><span class="w"></span>

<span class="k">impl</span><span class="w"> </span><span class="n">Foo</span><span class="w"> </span><span class="k">for</span><span class="w"> </span><span class="kt">i32</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="k">type</span> <span class="nc">Assoc</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="kt">u32</span><span class="p">;</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>

<span class="k">fn</span> <span class="nf">main</span><span class="p">()</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">fun1</span>::<span class="o">&lt;</span><span class="kt">i32</span><span class="o">&gt;</span><span class="p">();</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>



<a name="231491554"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491554" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491554">(Mar 23 2021 at 15:39)</a>:</h4>
<p><span class="user-mention silent" data-user-id="121053">varkor</span> <a href="#narrow/stream/260443-project-const-generics/topic/meeting.202021-03-23/near/231491506">said</a>:</p>
<blockquote>
<p>It also seems likely that without a formally verified model of trait solving, it's likely these issues will be hit again and again. Maybe you can tempt an academic into working on it.</p>
</blockquote>
<p>side note that</p>



<a name="231491571"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491571" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491571">(Mar 23 2021 at 15:39)</a>:</h4>
<p>I'm talking to some folks about an interesting idea that is very much related here</p>



<a name="231491600"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491600" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491600">(Mar 23 2021 at 15:39)</a>:</h4>
<p>we've been talking about taking the chalk formalization of trait semantics</p>



<a name="231491623"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491623" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491623">(Mar 23 2021 at 15:39)</a>:</h4>
<p>combined with polonius definition of the borrow checker</p>



<a name="231491641"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491641" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491641">(Mar 23 2021 at 15:39)</a>:</h4>
<p>and a (to be written) formal type checker for MIR</p>



<a name="231491685"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491685" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491685">(Mar 23 2021 at 15:39)</a>:</h4>
<p>at this point you have a complete type checker for MIR that is based entirely on horn clauses</p>



<a name="231491743"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491743" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491743">(Mar 23 2021 at 15:40)</a>:</h4>
<p>I'd be very interested in hearing more about that.</p>



<a name="231491771"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491771" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491771">(Mar 23 2021 at 15:40)</a>:</h4>
<p>That seems like the right way to go.</p>



<a name="231491778"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491778" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Boxy [she/her] <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491778">(Mar 23 2021 at 15:40)</a>:</h4>
<p><span aria-label="eyes" class="emoji emoji-1f440" role="img" title="eyes">:eyes:</span></p>



<a name="231491810"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491810" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491810">(Mar 23 2021 at 15:40)</a>:</h4>
<p>the hope is that you can remove the rather artificial barriers we've placed between them</p>



<a name="231491841"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491841" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491841">(Mar 23 2021 at 15:40)</a>:</h4>
<p>and basically just give that whole bundle to the solver and say "solve this"</p>



<a name="231491909"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491909" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491909">(Mar 23 2021 at 15:41)</a>:</h4>
<p>but also that we can use it as the basis for proving soundness of a MIR analysis</p>



<a name="231491921"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491921" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491921">(Mar 23 2021 at 15:41)</a>:</h4>
<p>modulo unsafe code, of course :)</p>



<a name="231491954"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231491954" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231491954">(Mar 23 2021 at 15:41)</a>:</h4>
<p>(so this brings us back to <span class="user-mention" data-user-id="120791">@RalfJ</span>'s thesis, somewhat)</p>



<a name="231492027"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492027" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492027">(Mar 23 2021 at 15:41)</a>:</h4>
<p>(since the point of his approach was to give a way to model unsafe code as well, with some of the proof obligations falling on the author of the code)</p>



<a name="231492097"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492097" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492097">(Mar 23 2021 at 15:42)</a>:</h4>
<p>ooh</p>



<a name="231492166"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492166" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492166">(Mar 23 2021 at 15:42)</a>:</h4>
<p>I was talking to some folks in amazon's automated reasoning group about this</p>



<a name="231492187"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492187" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492187">(Mar 23 2021 at 15:42)</a>:</h4>
<p>it seems pretty appealing as a project to undertake</p>



<a name="231492224"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492224" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492224">(Mar 23 2021 at 15:43)</a>:</h4>
<p>note <span class="user-mention" data-user-id="232957">@Jack Huey</span> that it also sidesteps the question of recursive vs SLG solver somewhat</p>



<a name="231492237"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492237" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492237">(Mar 23 2021 at 15:43)</a>:</h4>
<p>Even safety of type checking alone would be a big step forward. Integrating safety checking at the expression-level too would be even better.</p>



<a name="231492282"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492282" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492282">(Mar 23 2021 at 15:43)</a>:</h4>
<p>in particular you want a solver more like the SLG one for this -- though maybe not the SLG solver -- that is, you want a complete solver</p>



<a name="231492356"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492356" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492356">(Mar 23 2021 at 15:43)</a>:</h4>
<p>the main insight that hadn't occurred to me before</p>



<a name="231492377"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492377" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492377">(Mar 23 2021 at 15:43)</a>:</h4>
<p>was that doing this at the MIR level is totally tractable</p>



<a name="231492431"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492431" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492431">(Mar 23 2021 at 15:44)</a>:</h4>
<p>whereas doing it for rust source code feels absurd right now</p>



<a name="231492541"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492541" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492541">(Mar 23 2021 at 15:44)</a>:</h4>
<p>to circle back to the topic at hand, I think this is a mildly simplified example of the problem, right <span class="user-mention" data-user-id="216206">@lcnr</span> ?</p>



<a name="231492551"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492551" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492551">(Mar 23 2021 at 15:44)</a>:</h4>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">trait</span><span class="w"> </span><span class="n">Foo</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="k">type</span> <span class="nc">Assoc</span><span class="p">;</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>

<span class="k">const</span><span class="w"> </span><span class="k">fn</span> <span class="nf">bar</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">()</span><span class="w"></span>
<span class="k">where</span><span class="w"></span>
<span class="w">    </span><span class="n">T</span>: <span class="nc">Foo</span><span class="o">&lt;</span><span class="n">Assoc</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">T</span><span class="o">&gt;</span><span class="p">,</span><span class="w"></span>
<span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="o">..</span><span class="p">.</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>

<span class="k">fn</span> <span class="nf">fun1</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"></span>
<span class="k">where</span><span class="w"></span>
<span class="w">    </span><span class="n">T</span>: <span class="nc">Foo</span><span class="o">&lt;</span><span class="n">Assoc</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">T</span><span class="o">&gt;</span><span class="p">,</span><span class="w"></span>
<span class="w">    </span><span class="p">[</span><span class="kt">u8</span><span class="p">;</span><span class="w"> </span><span class="n">bar</span>::<span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">()]</span>: <span class="nb">Sized</span><span class="p">,</span><span class="w"></span>
<span class="p">{}</span><span class="w"></span>

<span class="k">impl</span><span class="w"> </span><span class="n">Foo</span><span class="w"> </span><span class="k">for</span><span class="w"> </span><span class="kt">i32</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="k">type</span> <span class="nc">Assoc</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="kt">u32</span><span class="p">;</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>

<span class="k">fn</span> <span class="nf">main</span><span class="p">()</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">fun1</span>::<span class="o">&lt;</span><span class="kt">i32</span><span class="o">&gt;</span><span class="p">();</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>



<a name="231492620"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492620" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492620">(Mar 23 2021 at 15:45)</a>:</h4>
<p>in particular, the problem is that the where clauses on the call to <code>bar::&lt;T&gt;()</code> are assumed to be satisfied</p>



<a name="231492628"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492628" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492628">(Mar 23 2021 at 15:45)</a>:</h4>
<p>ye</p>



<a name="231492649"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492649" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492649">(Mar 23 2021 at 15:45)</a>:</h4>
<p>and we may evaluate it under that assumption</p>



<a name="231492652"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492652" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492652">(Mar 23 2021 at 15:45)</a>:</h4>
<p>that has the same issue</p>



<a name="231492655"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492655" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492655">(Mar 23 2021 at 15:45)</a>:</h4>
<p>which may turn out to be untrue</p>



<a name="231492834"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492834" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492834">(Mar 23 2021 at 15:46)</a>:</h4>
<p>even <code>bar&lt;T: Sized&gt;()</code> is probably enough</p>



<a name="231492878"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492878" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492878">(Mar 23 2021 at 15:46)</a>:</h4>
<p>with <code>fun1::&lt;[i32]&gt;()</code> in main</p>



<a name="231492954"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231492954" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Boxy [she/her] <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231492954">(Mar 23 2021 at 15:47)</a>:</h4>
<p>so, this is only problematic because of const generics allowing for actaully evaluating code which can observe the fact that we incorrectly assume the predicate holds?</p>



<a name="231493029"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231493029" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231493029">(Mar 23 2021 at 15:47)</a>:</h4>
<p>that's my understanding, yes</p>



<a name="231493115"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231493115" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231493115">(Mar 23 2021 at 15:48)</a>:</h4>
<p>I think that's true</p>



<a name="231493177"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231493177" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231493177">(Mar 23 2021 at 15:48)</a>:</h4>
<p>we would otherwise eventually fail to prove something</p>



<a name="231493205"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231493205" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231493205">(Mar 23 2021 at 15:48)</a>:</h4>
<p>let me write my write-up into the hackmd</p>



<a name="231493230"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231493230" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231493230">(Mar 23 2021 at 15:48)</a>:</h4>
<p>I just sent some messages to some people to see if they had any insights</p>



<a name="231493247"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231493247" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231493247">(Mar 23 2021 at 15:48)</a>:</h4>
<p>and I <em>thought</em> I did a crisp job articulating it :)</p>



<a name="231493586"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231493586" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231493586">(Mar 23 2021 at 15:50)</a>:</h4>
<p><a href="https://hackmd.io/ApIfCRWSQEa0insNCkNZ-w#ICE-example">done</a></p>



<a name="231493923"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231493923" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231493923">(Mar 23 2021 at 15:52)</a>:</h4>
<p>we could try to change <code>bug</code>s in ctfe to <code>if param_env.reveal() == Reveal::Selection { return Err(BrokenAssumption) } else { bug!(...) }</code> which makes the first option slightly less scary to me (after <a href="https://github.com/rust-lang/rust/issues/81339">#81339</a>)</p>



<a name="231494058"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231494058" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231494058">(Mar 23 2021 at 15:53)</a>:</h4>
<p>i would still prefer to "cleanly" solve this</p>



<a name="231494455"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231494455" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231494455">(Mar 23 2021 at 15:55)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> <a href="#narrow/stream/260443-project-const-generics/topic/meeting.202021-03-23/near/231493230">said</a>:</p>
<blockquote>
<p>I just sent some messages to some people to see if they had any insights</p>
</blockquote>
<p>maybe we can get some additional helpful input here</p>



<a name="231496673"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231496673" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231496673">(Mar 23 2021 at 16:06)</a>:</h4>
<p>i had another idea rn</p>



<a name="231496763"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231496763" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231496763">(Mar 23 2021 at 16:07)</a>:</h4>
<ul>
<li>only evaluate anon const if they are fully concrete</li>
</ul>



<a name="231496802"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231496802" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Boxy [she/her] <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231496802">(Mar 23 2021 at 16:07)</a>:</h4>
<p>uh</p>



<a name="231496804"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231496804" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231496804">(Mar 23 2021 at 16:07)</a>:</h4>
<ul>
<li>before evaluating the anon const, check its caller bounds hold in an empty param env</li>
</ul>



<a name="231496829"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231496829" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Boxy [she/her] <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231496829">(Mar 23 2021 at 16:07)</a>:</h4>
<p>how would you evaluate an anon const if it isnt concrete?</p>



<a name="231496952"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231496952" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231496952">(Mar 23 2021 at 16:08)</a>:</h4>
<p>we sometimes still try to evaluate generic constants, i think we do it because we currently can't deal with unused substs</p>



<a name="231496971"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231496971" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Boxy [she/her] <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231496971">(Mar 23 2021 at 16:08)</a>:</h4>
<p>oh</p>



<a name="231496977"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231496977" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Boxy [she/her] <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231496977">(Mar 23 2021 at 16:08)</a>:</h4>
<p>that</p>



<a name="231497040"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231497040" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Boxy [she/her] <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231497040">(Mar 23 2021 at 16:08)</a>:</h4>
<p>we could really do with an actual way of checking concreteness lmao</p>



<a name="231497067"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231497067" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Boxy [she/her] <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231497067">(Mar 23 2021 at 16:08)</a>:</h4>
<p>slash yeeting unused substs</p>



<a name="231497083"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231497083" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231497083">(Mar 23 2021 at 16:09)</a>:</h4>
<p>or maybe because it did not cause any issues and more cleanly fit into the mental model of the people first implementing it</p>



<a name="231508609"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/260443-project-const-generics/topic/meeting%202021-03-23/near/231508609" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/260443-project-const-generics/topic/meeting.202021-03-23.html#231508609">(Mar 23 2021 at 17:18)</a>:</h4>
<p><span class="user-mention silent" data-user-id="121053">varkor</span> <a href="#narrow/stream/260443-project-const-generics/topic/meeting.202021-03-23/near/231491318">said</a>:</p>
<blockquote>
<p>It would be nice to have a document in the project-const-generics repo, or elsewhere, that lists all these problem cases that have been encountered, so there's a good reference to point people towards in the future.</p>
</blockquote>
<p>opened <a href="https://github.com/rust-lang/project-const-generics/pull/10">https://github.com/rust-lang/project-const-generics/pull/10</a></p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>